The category of classes has classes as objects and maps of classes as morphisms.
In the Zermelo-Fraenkel set theory, a class is a proposition with a designated free variable . We interpret as saying that belongs to the class . We also write , while understanding that is not a set, but is.
For example, any set is a class, whose proposition is and the designated free variable is .
The proposition defines the class of all sets, which does not arise via the above construction from any set.
Given two classes and , we can form their product as the class such that means for some and , where denotes the usual ordered pair constructed in Zermelo-Fraenkel set theory as or or .
If implies , we say that is a subclass of .
A relation from to is a subclass of .
A map from to is a relation from to such that for any there is a unique such that . In this case we write for this unique , so means .
Maps of classes can be composed in the usual manner, which produces a category.
Here a category is understood in the sense of a first-order logic with two sorts (objects and morphisms), but at no point we attempt to consider all classes as a single unified whole.
A family of classes indexed by a class is a map of classes . The class indexed by is the preimage . Such families can be pulled back along maps of classes and pushed forward along maps .
We can now define large categories as having a class of objects, a class of morphisms, together with composition and identities satisfying the usual axioms. The category of classes considered above is not a large category in this sense.
We do not require large categories to be locally small.
Suppose is a large category. An -indexed diagram of classes is defined as follows. First, we have an -indexed family of classes . Secondly, we have a transition map
which is a map of classes such that . (The domain of is a class because and are sets.) Finally, the transition map satisfies the usual axioms expected from a functor.
For any large category and a class we can define the constant diagram indexed by with value . We take with being the projection map. The transition map sends .
For any large category we have a constant diagram functor that sends a class to the constant diagram on .
We can talk about left and right adjoint functors to this functor in the sense of a first-order logic with two sorts (objects and morphisms), augmented with symbols for the functor, its adjoint, together with unit and counit maps that satisfy the triangle identities.
The category of classes admits all small limits.
First, it admits equalizers: the equalizer of is the subclass of defined by .
Secondly, it admits small products: the small product of an -indexed family of classes , where is an arbitrary set (considered as a class when used with ) can be constructed as the class such that if is a map of sets? whose domain is and for all we have and . (Observe that is indeed a class.)
Finally, it admits all small limits because the usual reduction of small limits to equalizers of small products continues to work provided that we adhere to the above convention on the definition of families of classes.
The category of classes admits all colimits indexed by arbitrary large categories , i.e., large colimits.
First, the standard reduction of -indexed colimits to a coequalizer of a pair of arrows between coproducts indexed by and still works in this context since class-indexed families of classes can be pulled back along source and target maps .
Secondly, class-indexed coproducts of classes can be computed simply by taking the total class of the corresponding class-indexed family of classes.
Thirdly, coequalizers of classes exist by Scott's trick. Observe that given a pair of arrows between classes, we can define an equivalence relation on by saying that if there is a map such that , and for any there is such that and or and . The quotient of by this equivalence relation exists by Scott's trick and is precisely the desired coequalizer.
The category of classes is a regular category: the obvious notion of image factorization is stable under pullbacks. It is also a Barr-exact category: every equivalence relation on a class is induced by the quotient map .
It is also an infinitary extensive category, where “infinitary” means “class-indexed”. Indeed, pullbacks of coproduct injections along arbitrary maps of classes exist and class-indexed coproducts are disjoint and stable under pullback.
It is also well-pointed: for every two maps between classes and every element , if , then , and the category of classes is not the terminal category.
It likewise has all objects corresponding to large cardinals, most notably a natural numbers object. Otherwise, the category of finite sets FinSet is vacuously a category of classes, as the notions of ‘finitary’ and ‘class-indexed’/‘infinitary’ coincide.
As such, the category of classes is a well-pointed infinitary Heyting or Boolean pretopos, depending upon the external logic used, with a natural numbers object and other large cardinals, and where “infinitary” is used in the rather strong sense of “class-indexed”.
The category of classes is not cartesian closed or locally cartesian closed and does not have power objects. Indeed, the class of all sets does not have a power object, or, equivalently, there is no internal hom .
The category of classes is a primordial example of a category with class structure. Its open maps are precisely those maps of classes such that is a set for each . Small maps coincide with open maps. The powerclass of a class is the class of all sets such that is a subclass of . The universal class is the class of all sets.
Last revised on July 22, 2023 at 14:50:18. See the history of this page for a list of all contributions to it.